$\forall$$E$, $A$:Type, ${\it info}$:($E$$\rightarrow$(Id$\times$$A$+(IdLnk$\times$$E$)$\times$Id)), $e$:$E$. rcv?($e$) $\Rightarrow$ rtag(${\it info}$;$e$) $\in$ Id